ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), es:ES, i:Id.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  Valtype(da;kind(e)))
 (m:. ecl-es-act(es;m;x)  {e:E| loc(e) = i }{e:E| loc(e) = i }Prop) 

latex

Definitions

x:A. B(x), P  Q, , t  T, Prop, ecl-es-act(es;m;x), False, P  Q, P & Q, A, if b t else f fi, x,y. t(x;y), x,y,z,w. t(x;y;z;w), A & B, x. t(x), AB, S  T, x,y,z. t(x;y;z), true, false, , x(s1,s2), x(s1,s2,s3,s4), x(s1,s2,s3), x(s), , Unit, P  Q,

Lemmas

ecl ind wf, es-loc wf, false wf, decl-state wf, ma-valtype wf, bool wf, ecl-es-halt wf, existse-between3 wf, not wf, assert wf, es-first wf, es-pred wf, es-loc-pred, l-all wf, nat plus wf, ecl-ex wf, alle-between1 wf, le wf, l member wf, nat plus inc, nat wf, es-pstar-q wf, iff transitivity, eqtt to assert, assert of eq int, bnot wf, eqff to assert, assert of bnot, not functionality wrt iff, es-E wf, Id wf, es-valtype wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, ecl wf, fpf wf, Knd wf